0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 1 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 MRRProof (⇔, 24 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
plusB_in_gaa(0, T5, T5) → plusB_out_gaa(0, T5, T5)
plusB_in_gaa(s(0), T20, s(T20)) → plusB_out_gaa(s(0), T20, s(T20))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U2_gaa(T23, T12, T13, pA_in_ga(T23, X31))
pA_in_ga(s(T27), s(X40)) → U1_ga(T27, X40, pA_in_ga(T27, X40))
U1_ga(T27, X40, pA_out_ga(T27, X40)) → pA_out_ga(s(T27), s(X40))
U2_gaa(T23, T12, T13, pA_out_ga(T23, X31)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U3_gaa(T23, T12, T13, pA_in_ga(T23, T24))
U3_gaa(T23, T12, T13, pA_out_ga(T23, T24)) → U4_gaa(T23, T12, T13, plusB_in_gaa(s(s(T24)), T12, T13))
U4_gaa(T23, T12, T13, plusB_out_gaa(s(s(T24)), T12, T13)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
plusB_in_gaa(0, T5, T5) → plusB_out_gaa(0, T5, T5)
plusB_in_gaa(s(0), T20, s(T20)) → plusB_out_gaa(s(0), T20, s(T20))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U2_gaa(T23, T12, T13, pA_in_ga(T23, X31))
pA_in_ga(s(T27), s(X40)) → U1_ga(T27, X40, pA_in_ga(T27, X40))
U1_ga(T27, X40, pA_out_ga(T27, X40)) → pA_out_ga(s(T27), s(X40))
U2_gaa(T23, T12, T13, pA_out_ga(T23, X31)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U3_gaa(T23, T12, T13, pA_in_ga(T23, T24))
U3_gaa(T23, T12, T13, pA_out_ga(T23, T24)) → U4_gaa(T23, T12, T13, plusB_in_gaa(s(s(T24)), T12, T13))
U4_gaa(T23, T12, T13, plusB_out_gaa(s(s(T24)), T12, T13)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
PLUSB_IN_GAA(s(s(T23)), T12, s(T13)) → U2_GAA(T23, T12, T13, pA_in_ga(T23, X31))
PLUSB_IN_GAA(s(s(T23)), T12, s(T13)) → PA_IN_GA(T23, X31)
PA_IN_GA(s(T27), s(X40)) → U1_GA(T27, X40, pA_in_ga(T27, X40))
PA_IN_GA(s(T27), s(X40)) → PA_IN_GA(T27, X40)
PLUSB_IN_GAA(s(s(T23)), T12, s(T13)) → U3_GAA(T23, T12, T13, pA_in_ga(T23, T24))
U3_GAA(T23, T12, T13, pA_out_ga(T23, T24)) → U4_GAA(T23, T12, T13, plusB_in_gaa(s(s(T24)), T12, T13))
U3_GAA(T23, T12, T13, pA_out_ga(T23, T24)) → PLUSB_IN_GAA(s(s(T24)), T12, T13)
plusB_in_gaa(0, T5, T5) → plusB_out_gaa(0, T5, T5)
plusB_in_gaa(s(0), T20, s(T20)) → plusB_out_gaa(s(0), T20, s(T20))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U2_gaa(T23, T12, T13, pA_in_ga(T23, X31))
pA_in_ga(s(T27), s(X40)) → U1_ga(T27, X40, pA_in_ga(T27, X40))
U1_ga(T27, X40, pA_out_ga(T27, X40)) → pA_out_ga(s(T27), s(X40))
U2_gaa(T23, T12, T13, pA_out_ga(T23, X31)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U3_gaa(T23, T12, T13, pA_in_ga(T23, T24))
U3_gaa(T23, T12, T13, pA_out_ga(T23, T24)) → U4_gaa(T23, T12, T13, plusB_in_gaa(s(s(T24)), T12, T13))
U4_gaa(T23, T12, T13, plusB_out_gaa(s(s(T24)), T12, T13)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
PLUSB_IN_GAA(s(s(T23)), T12, s(T13)) → U2_GAA(T23, T12, T13, pA_in_ga(T23, X31))
PLUSB_IN_GAA(s(s(T23)), T12, s(T13)) → PA_IN_GA(T23, X31)
PA_IN_GA(s(T27), s(X40)) → U1_GA(T27, X40, pA_in_ga(T27, X40))
PA_IN_GA(s(T27), s(X40)) → PA_IN_GA(T27, X40)
PLUSB_IN_GAA(s(s(T23)), T12, s(T13)) → U3_GAA(T23, T12, T13, pA_in_ga(T23, T24))
U3_GAA(T23, T12, T13, pA_out_ga(T23, T24)) → U4_GAA(T23, T12, T13, plusB_in_gaa(s(s(T24)), T12, T13))
U3_GAA(T23, T12, T13, pA_out_ga(T23, T24)) → PLUSB_IN_GAA(s(s(T24)), T12, T13)
plusB_in_gaa(0, T5, T5) → plusB_out_gaa(0, T5, T5)
plusB_in_gaa(s(0), T20, s(T20)) → plusB_out_gaa(s(0), T20, s(T20))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U2_gaa(T23, T12, T13, pA_in_ga(T23, X31))
pA_in_ga(s(T27), s(X40)) → U1_ga(T27, X40, pA_in_ga(T27, X40))
U1_ga(T27, X40, pA_out_ga(T27, X40)) → pA_out_ga(s(T27), s(X40))
U2_gaa(T23, T12, T13, pA_out_ga(T23, X31)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U3_gaa(T23, T12, T13, pA_in_ga(T23, T24))
U3_gaa(T23, T12, T13, pA_out_ga(T23, T24)) → U4_gaa(T23, T12, T13, plusB_in_gaa(s(s(T24)), T12, T13))
U4_gaa(T23, T12, T13, plusB_out_gaa(s(s(T24)), T12, T13)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
PA_IN_GA(s(T27), s(X40)) → PA_IN_GA(T27, X40)
plusB_in_gaa(0, T5, T5) → plusB_out_gaa(0, T5, T5)
plusB_in_gaa(s(0), T20, s(T20)) → plusB_out_gaa(s(0), T20, s(T20))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U2_gaa(T23, T12, T13, pA_in_ga(T23, X31))
pA_in_ga(s(T27), s(X40)) → U1_ga(T27, X40, pA_in_ga(T27, X40))
U1_ga(T27, X40, pA_out_ga(T27, X40)) → pA_out_ga(s(T27), s(X40))
U2_gaa(T23, T12, T13, pA_out_ga(T23, X31)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U3_gaa(T23, T12, T13, pA_in_ga(T23, T24))
U3_gaa(T23, T12, T13, pA_out_ga(T23, T24)) → U4_gaa(T23, T12, T13, plusB_in_gaa(s(s(T24)), T12, T13))
U4_gaa(T23, T12, T13, plusB_out_gaa(s(s(T24)), T12, T13)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
PA_IN_GA(s(T27), s(X40)) → PA_IN_GA(T27, X40)
PA_IN_GA(s(T27)) → PA_IN_GA(T27)
From the DPs we obtained the following set of size-change graphs:
PLUSB_IN_GAA(s(s(T23)), T12, s(T13)) → U3_GAA(T23, T12, T13, pA_in_ga(T23, T24))
U3_GAA(T23, T12, T13, pA_out_ga(T23, T24)) → PLUSB_IN_GAA(s(s(T24)), T12, T13)
plusB_in_gaa(0, T5, T5) → plusB_out_gaa(0, T5, T5)
plusB_in_gaa(s(0), T20, s(T20)) → plusB_out_gaa(s(0), T20, s(T20))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U2_gaa(T23, T12, T13, pA_in_ga(T23, X31))
pA_in_ga(s(T27), s(X40)) → U1_ga(T27, X40, pA_in_ga(T27, X40))
U1_ga(T27, X40, pA_out_ga(T27, X40)) → pA_out_ga(s(T27), s(X40))
U2_gaa(T23, T12, T13, pA_out_ga(T23, X31)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
plusB_in_gaa(s(s(T23)), T12, s(T13)) → U3_gaa(T23, T12, T13, pA_in_ga(T23, T24))
U3_gaa(T23, T12, T13, pA_out_ga(T23, T24)) → U4_gaa(T23, T12, T13, plusB_in_gaa(s(s(T24)), T12, T13))
U4_gaa(T23, T12, T13, plusB_out_gaa(s(s(T24)), T12, T13)) → plusB_out_gaa(s(s(T23)), T12, s(T13))
PLUSB_IN_GAA(s(s(T23)), T12, s(T13)) → U3_GAA(T23, T12, T13, pA_in_ga(T23, T24))
U3_GAA(T23, T12, T13, pA_out_ga(T23, T24)) → PLUSB_IN_GAA(s(s(T24)), T12, T13)
pA_in_ga(s(T27), s(X40)) → U1_ga(T27, X40, pA_in_ga(T27, X40))
U1_ga(T27, X40, pA_out_ga(T27, X40)) → pA_out_ga(s(T27), s(X40))
PLUSB_IN_GAA(s(s(T23))) → U3_GAA(pA_in_ga(T23))
U3_GAA(pA_out_ga(T24)) → PLUSB_IN_GAA(s(s(T24)))
pA_in_ga(s(T27)) → U1_ga(pA_in_ga(T27))
U1_ga(pA_out_ga(X40)) → pA_out_ga(s(X40))
pA_in_ga(x0)
U1_ga(x0)
PLUSB_IN_GAA(s(s(T23))) → U3_GAA(pA_in_ga(T23))
U3_GAA(pA_out_ga(T24)) → PLUSB_IN_GAA(s(s(T24)))
pA_in_ga(s(T27)) → U1_ga(pA_in_ga(T27))
U1_ga(pA_out_ga(X40)) → pA_out_ga(s(X40))
pAinga1 > U1ga1 > pAoutga1 > U3GAA1 > PLUSBINGAA1 > s1
pA_in_ga_1=1
s_1=3
U1_ga_1=3
pA_out_ga_1=2
PLUSB_IN_GAA_1=1
U3_GAA_1=5
pA_in_ga(x0)
U1_ga(x0)